

We need the following auxiliary definitions.

\begin{definition}
Given two \evol{} processes in normal form $P$ and $Q$, 
we define $\CStr(P \parallel Q)$ as follows.
The root is labeled $\epsilon$, and has $n+m$ children: 
the first $n$ sub-children correspond to the children of the root of $\CStr(P)$,
while the rest correspond to the $m$ children of the root of $\CStr(Q)$,
\end{definition}


%The following proposition provides conditions for 

\begin{proposition}[Syntactic Closure for \evols{} processes]\label{prop:howstatic}
Let $P_{1}, P_{2}, \ldots$ be \evol{} processes.
\begin{enumerate}
 \item $P_1, P_2 \in \evols{}$ iff $P_1 \parallel P_2 \in \evols{}$.
 \item $P \in \evols{}$ iff $\component{a}{P} \in \evols{}$.
 \item $P_i \in \evols{}$  and $\numap{P_i} =0$ for $i\in [1..n]$  iff $\sum_{i=1}^n \pi_i.P_i \in \evols{}.$
 \item $P \in \evols{}$  and $\numap{P} =0$  iff $! \pi.P \in \evols{}.$
\end{enumerate}
\end{proposition}

\begin{proof}
Immediate from Definitions \ref{d:eccsstatic} and \ref{d:numap}.
In particular, items (3) and (4) follow  by observing that 
any process $P$ such that $\numap{P}=0$ belongs to the syntactic category $A$ in the grammar of \evols{} processes given in 
Definition \ref{d:eccsstatic}.
\end{proof}

We repeat the statement in Page \pageref{l:esred}:
\begin{lemma}
Let $P$ be an \evols{} process.
If $P \pired P'$ then
also $P'$ is an  \evols{} process. Moreover, $\CStr(P)=\CStr(P')$.
\end{lemma}
\begin{proof}

The proof proceeds by induction on the height of the derivation tree for $P \pired P'$, with a case analysis on the last applied rule. 
There are seven cases to check. 
%We detail only cases for rules \rulename{Act1}, \rulename{Loc}, \rulename{Tau1}, and \rulename{Tau3}; the remaining cases are similar or simpler.

\begin{description}
\item[Case \rulename{Act1}]
Then $P = P_{1} \parallel P_{2}$ and $P' = P'_{1} \parallel P_{2}$, with $P_{1} \pired P'_{1}$.
By inductive hypothesis, we have that $P'_{1}$ is an \evols{} process. By Proposition \ref{prop:howstatic} we have that $P_2 \in \evols{}$, and we can therefore conclude that $P' = P'_{1} \parallel P_{2}$ is an \evols{} process.

Moreover, by inductive hypothesis, we have that  $\CStr(P_{1}) = \CStr(P'_{1})$ and 
 by Definition \ref{def:cstr} it is easy to see that  
 $\CStr(P_{1} \parallel P_{2}) = \CStr(P'_{1} \parallel P_{2})$ holds.

 \item [Case \rulename{Act2}:] Analogous to the case for \rulename{Act1} and omitted. 

\item[Case \rulename{Loc}] 
Then $P = \component{a}{Q}$ and $P' = \component{a}{Q'}$, with $Q \pired Q'$.
By inductive hypothesis, we have that $Q'$ is an \evols{} process. For Proposition \ref{prop:howstatic} we have that $P' = \component{a}{Q'}$ is an \evols{} process. 

Moreover, by inductive hypothesis, we have that $\CStr(Q) = \CStr(Q')$.
Then, it is immediate to see that by Definition  \ref{def:cstr} 
$\CStr(\component{a}{Q}) = \CStr(\component{a}{Q'})$.


\item [Cases \rulename{Tau1}-\rulename{Tau2}:]
Then $P \equiv  \fillcont{C_1}{A}\parallel \fillcont{C_2}{B}$, where $C_{1}, C_{2}$ are monadic contexts as in Definition \ref{d:mc}.
Moreover, 
$A$ is either 
$!b.Q$ or 
$\sum_{i \in I} \pi_i.Q_i$ with $\pi_{l}=b$, for some $l\in I$, and 
$B$ is either 
$!\outC{b}.R$
or $\sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\outC{b}$, for some $l\in I$.

We consider only the case in which $A = \sum_{i \in I} \pi_i.Q_i$ and $B = !\outC{b}.R$;  the other cases are similar. 
Then $P' \equiv \fillcont{C_1}{Q_l}\parallel \fillcont{C_2}{R \parallel!\outC{b}.R }$ and from Proposition \ref{prop:howstatic} we easily conclude that $P'$ is an \evols{} process.


By assumption and by Proposition \ref{prop:howstatic}  we have that $A$ and $B$ are \evols{} processes. In turn, this allows us to infer that 
 $\CStr(\sum_{i \in I} \pi_i.Q_i) = \CStr(Q'_{l})$
 and
  $\CStr( !\outC{b}.R) = \CStr(R)$, as well-formed \evols{} processes do not contain adaptable processes behind prefixes, 
  and therefore their component structure denotations are unaffected by input/output transitions.
  The thesis then follows by Definition \ref{def:cstr}: $\CStr(P) = \CStr(P')$.


\item [Cases \rulename{Tau3}-\rulename{Tau4}:]
Then $P \equiv \fillcont{C_1}{A} \parallel \fillcont{C_2}{B}$ where:
\begin{itemize}
\item $C_{1},C_{2}$ are monadic contexts, as in Definition \ref{d:mc}; 
\item $A = \component{b}{P_1}$, for some $P_{1}$;  
\item $B  =  \sum_{i \in I} \pi_i.R_i$ with $\pi_{l}=\update{b}{\component{b}{U} \parallel P_2}$ for $l\in I$, or $ B = !\update{b}{\component{b}{U} \parallel P_2}.R$, for some $P_{2}, R$.
\end{itemize}

We consider the case in which $B = !\update{b}{\component{b}{U} \parallel P_2}.R$; the other case is similar. 
Then $P' \equiv \fillcont{C_1}{\component{a}{\fillcon{U}{P_1}} \parallel P_2}\parallel \fillcont{C_2}{R \parallel !\update{b}{\component{b}{U} \parallel P_2}.R }$.
For Proposition \ref{prop:howstatic} we have that $\fillcont{C_2}{R \parallel !\update{b}{\component{b}{U} \parallel P_2}.R }$  and $P_2$ are \evols{} processes. We now focus on process $\fillcon{U}{P_1}$, for Proposition \ref{prop:howstatic} we know that $P_1$ is an \evols{} process, if $\numph{U} = 0$ then it could not occur that an adaptable process in $P_1$ is prefixed.   Otherwise, if $\numph{U} > 0$ then the side condition (2) of rule \rulename{Tau3}(\rulename{Tau4}) ensures that $\numap{P_1} = 0$. As $U$ follows the syntax of \evols{} by means of Proposition \ref{prop:howstatic}
we can conclude that $\fillcon{U}{P_1} \in \evols{}$.

Moreover, the side condition (1) of rule \rulename{Tau3}(\rulename{Tau4}) implies that  $$\CStr( \component{b}{P_1}) = \CStr(\component{a}{\fillcon{U}{P_1}} \parallel P_2).$$   The thesis then follows by Definition \ref{def:cstr}: $\CStr(P) = \CStr(P')$.
\end{description}
\end{proof}